Solution to challenge 15, via cryspen-ext/core-models

Resolves model-checking#173

This PR provides testable models for core::arch intrinsics, including abstractions to streamline the process of implementing these intrinsics and their tests.

Currently there are 256 x86 intrinsics modelled, and 181 aarch64 intrinsics modelled.

The methodology for writing the models is decribed in testable-simd-models/README.md.
First, we model the SIMD types as bitvectors that can be converted to and from arrays of machine integers.
Then, we model the raw operations on these types as functions over bitvectors, while keeping as much code as possible unchanged from the Rust code in rust-lang/stdarch/crates/core_arch.
Finally, we write tests (using a generic macro) to compare the behaviour of our models with the corresponding intrinsic implementations in Rust core.

Interestingly, in the process of modeling these intrinsivcs, we found bugs in the implementation of two intrinsics, _mm256_bsrli_epi128 and _mm512_bsrli_epi128. These bugs were fixed by our PR in the 2025-06-30 version of the library. In a small way, this shows off the impact of writing testable models of the SIMD intrinsics.

The model of intrinsics defined here is also used as the basis of formal proofs of Rust programs that use intrinsics. In particular, the libcrux cryptographic library uses these models in its proofs of the post-quantum cryptographic algorithms.

As next steps, we intend to extend these testable models to a larger subset of core (beyond SIMD) and then translate these Rust models to models in F*, Rocq, and Lean, to enable proofs using our models in these backends. This work is being done as part of the hax project.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.